Nuprl Definition : R-icompat 0,22

R-icompat(A;B)
== if Rplus?(A) R-icompat(Rplus-left(A);B) & R-icompat(Rplus-right(A);B)
== i; Rplus?(B) R-icompat(A;Rplus-left(B)) & R-icompat(A;Rplus-right(B))
== i; Rnone?(A) True
== i; Rnone?(B) True
== i; R-loc(A) = R-loc(B) True
== else R-interface-compat(A;B) & R-interface-compat(B;A) fi
(recursive) 
latex


DefinitionsY, x.A(x), Rplus?(x1), Rplus-left(x1), f(a), Rplus-right(x1), Rnone?(x1), if b t else f fi, a = b, R-loc(R), True, P & Q, R-interface-compat(A;B)
FDL editor aliasesR-icompat

origin